Inference at * 1 
Iof proof for Lemma can-apply-p-lift:



1. A : Type
2. B : Type
3. P : A
4. d : x:ADec(P(x))
5. f : {x:A| P(x)} B
6. x : A
  (isl(case d(x) of inl(a) => inl (f(x))  | inr(a) => inr a ))  P(x) 

latex

 by ((GenConclAtAddr [1;1;1;1]) 
CollapseTHENA (Auto)) 
CollapseTHEN ((D (-2)) 

CoCollapseTHEN ((Reduce 0) 
CollapseTHEN (Auto))) 

latex

C.

Definitions	, s = t, x:AB(x), x:A. B(x), Dec(P), P  Q, left + right, True, b, P  Q, P & Q, P  Q, x(s), f(a), t  T, A, P  Q, False
Lemmas	decidable wf, true wf, false wf